T:Type, f:(TT).
retraction(T;f)  (L:(T List), x, y, a, b:T. x=f*(y) via L  a before b  L  a = f+(b)) 

latex

Definitions	y = f+(x), P & Q, x:A  B(x), y is f*(x), x before y  l, y=f*(x) via L, type List, retraction(T;f), Type, False, P  Q, Void, s = t, x:A. B(x), x:AB(x), A, P  Q, P  Q, no_repeats(T;l), t  T,
Lemmas	false wf, fun-path-no repeats, no repeats wf, no repeats iff, not wf, fun-connected wf, strict-fun-connected wf, fun-path-before, l before wf, fun-path wf, retraction wf